Hugo Férée, Iris van der Giessen, Sam van Gool, Ian Shillito; "Mechanised uniform interpolation for modal logics K, GL and iSL"
Hugo Férée
,
Iris van der Giessen
,
Sam van Gool
,
Ian Shillito
https://arxiv.org/abs/2402.10494
正規様相論理K
,
証明可能性論理GL
,
直観主義証明可能性論理iGL
の
Uniform補間性
の証明及び
Coq
の形式化